basic
Refl(T;x,y.E(x;y)) == a:T. E(a;a) 

latex

Up	rel 1, rel 1
Wellformedness Lemmas	refl wf, refl wf
Definitions	x:A. B(x)
FDL editor aliases	refl